\begin{tabbing}
$\forall$\=$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:event\_system\{i:l\}, $x$:Id, $e$:\{\=$e$:es{-}E(${\it es}$)$\mid$ \+\+
\\[0ex]es{-}dtype(${\it es}$; loc($e$); $x$; $T$)\} ,
\-\\[0ex]$t$:rationals, ${\it e'}$:es{-}E(${\it es}$), $v$:$T$.
\-\\[0ex]($x$ unchanged{-}for $t$ @ $e$)
\\[0ex]$\Rightarrow$ @${\it e'}$($x$$\rightarrow$$v$)
\\[0ex]$\Rightarrow$ es{-}locl(${\it es}$; ${\it e'}$; $e$)
\\[0ex]$\Rightarrow$ qle((es{-}time(${\it es}$; ${\it e'}$) + $t$); es{-}time(${\it es}$; $e$))
\end{tabbing}